SherbyNet - /page/wikibook/entry.mu

Micron Document

<!DOCTYPE html>

<title>Program derivation</title>

</head>

<span id="openzim-page-title" class="mw-page-title-main"><span class="mw-page-title-main">Program derivation</span></span>

</h1>

</header>

<div id="mw-content-text" class="mw-body-content mw-content-ltr" lang="en" dir="ltr"><div class="mw-content-ltr mw-parser-output" lang="en" dir="ltr"><p>In <a href="Computer_science" title="Computer science">computer science</a>, <b>program derivation</b> is the derivation of a program from its specification, by mathematical means.

</p><p>To <i>derive</i> a program means to write a <a href="Formal_specification" title="Formal specification">formal specification</a>, which is usually non-executable, and then apply mathematically correct rules in order to obtain an <a href="Executable" title="Executable">executable</a> program satisfying that specification. The program thus obtained is then correct by construction. Program and <a href="Correctness_(computer_science)" title="Correctness (computer science)">correctness</a> proof are constructed together.

</p><p>The approach usually taken in <a href="Formal_verification" title="Formal verification">formal verification</a> is to first write a program, and then provide a <a href="Mathematical_proof" title="Mathematical proof">proof</a> that it conforms to a given <a href="Program_specification" class="mw-redirect" title="Program specification">specification</a>. The main problems with this are that:

</p>

<ul><li>the resulting proof is often long and cumbersome;</li>

<li>no insight is given as to how the program was developed; it appears "like a rabbit out of a hat";</li>

<li>should the program happen to be incorrect in some subtle way, the attempt to verify it is likely to be long and certain to be fruitless.</li></ul>

<p>Program derivation tries to remedy these shortcomings by:

</p>

<ul><li>keeping proofs shorter, by development of appropriate mathematical notations;</li>

<li>making design decisions through formal manipulation of the specification.</li></ul>

<p>Terms that are roughly synonymous with program derivation are: transformational programming, algorithmics, deductive programming.

</p><p>The <a href="Bird-Meertens_Formalism" class="mw-redirect" title="Bird-Meertens Formalism">Bird-Meertens Formalism</a> is an approach to program derivation.

</p><p>Approaches to achieving correctness in <a href="Distributed_computing" title="Distributed computing">Distributed computing</a> include research languages such as the <a href="P_(programming_language)" title="P (programming language)">P programming language</a>.

</p>

<ul><li><a href="Automatic_programming" title="Automatic programming">Automatic programming</a></li>

<li><a href="Hoare_logic" title="Hoare logic">Hoare logic</a></li>

<li><a href="Program_refinement" class="mw-redirect" title="Program refinement">Program refinement</a></li>

<li><a href="Design_by_contract" title="Design by contract">Design by contract</a></li>

<li><a href="Program_synthesis" title="Program synthesis">Program synthesis</a></li>

<li><a href="Proof-carrying_code" title="Proof-carrying code">Proof-carrying code</a></li></ul>

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

<ul><li><a href="Edsger_W._Dijkstra" title="Edsger W. Dijkstra">Edsger W. Dijkstra</a>, Wim H. J. Feijen, <i>A Method of Programming</i>, Addison-Wesley, 1988, 188 pages</li>

<li>Edward Cohen, <i>Programming in the 1990s</i>, Springer-Verlag, 1990</li>

<li>Anne Kaldewaij, <i>Programming: The Derivation of Algorithms</i>, Prentice-Hall, 1990, 216 pages</li>

<li>David Gries, <i>The Science of Programming</i>, Springer-Verlag, 1981, 350 pages</li>

<li><a href="Carroll_Morgan_(computer_scientist)" title="Carroll Morgan (computer scientist)">Carroll Morgan (computer scientist)</a>, <a rel="nofollow" class="external text" href="http://www.cs.ox.ac.uk/publications/books/PfS/"><i>Programming from Specifications</i></a>, International Series in Computer Science (2nd ed.), Prentice-Hall, 1998.</li>

<li><a href="Eric_Hehner" title="Eric Hehner">Eric C.R. Hehner</a>, <a rel="nofollow" class="external text" href="http://www.cs.toronto.edu/~hehner/aPToP/"><i>a Practical Theory of Programming</i></a>, 2008, 235 pages</li>

<li>A.J.M. van Gasteren. <i>On the Shape of Mathematical Arguments</i>. Lecture Notes in Computer Science #445, Springer-Verlag, 1990. Teaches how to write proofs with clarity and precision.</li>

<li>Martin Rem. "Small Programming Exercises", appeared in <i>Science of Computer Programming</i>, Vol.3 (1983) through Vol.14 (1990).</li>

<li>Roland Backhouse. <i>Program Construction: Calculating Implementations from Specifications</i>. Wiley, 2003. <style data-mw-deduplicate="TemplateStyles:r1238218222">

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0-470-84882-1</bdi>.</li>

<li>Derrick G. Kourie, Bruce W. Watson. <i>The Correctness-by-Construction Approach to Programming</i>. Springer-Verlag, 2012. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-3-642-27919-5</bdi>. Provides a step-by-step explanation of how to derive mathematically correct algorithms using small and tractable refinements.</li></ul></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2023-06-27" href="https://en.wikipedia.org/wiki/?title=Program_derivation&oldid=1162120704">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>